L:MsgA List. (A,BL.A ||+ B)  (L)  MsgA & (M:MsgA. (BL. M ||+ B)  (M ||+ (L))) 

latex

Definitions	x:A. B(x), t  T, P  Q, (x,yL.P(x;y)), A ||+ B, P & Q, (L), ||as||, reduce(f;k;as), Y, Prop, x. t(x), AB, A, False, x,y. t(x;y), {i..j}, x(s), i  j < k, P  Q, x(s1,s2), M1 || M2
Lemmas	msga wf, ma-empty wf, ma-empty-compatible-right, ma-empty-frame-compatible-right, l all wf, ma-compat wf, int seg wf, select wf, length wf2, pairwise-cons, ma-join wf, pairwise wf, l all cons, ma-compat-join